natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
The term higher-order abstract syntax has been used to refer to several distinct, but related, concepts. In chronological order, and from least to most generality:
Usage (1) does not appear to be in common usage. Usage (2) tends to be the convention in literature on logical frameworks; while usage (3) is the convention in literature on algebraic type theory, though note that authors often restrict to second-order abstract syntax?, which is sufficient for most type theories.
Examples of variable-binding operators are lambda-abstraction and quantifiers (e.g. in higher-order logic, whence the name).
In logical frameworks, one formalizes languages supporting forms of name binding (such as function parameters or quantifiers) by using the meta-language function space rather than a more syntactic notion of bound variable.
Traditional approaches to abstract syntax, e.g. for algebraic theories, typically involve abstract syntax trees. However, it is not possibly directly to capture variable-binding operators? with such structures. Therefore, alternative structures are necessary to capture the syntax of theories with such operators, e.g. type theories.
One possible approach is via the logical framework approach described above.
HOAS is used extensively in logical frameworks
Frank Pfenning, Conal Elliot, Higher-order abstract syntax, ACM SIGPLAN Notices 23 7 (1988) 199–208 [doi;10.1145/960116.54010, pdf]
Martin Hofmann, Semantical analysis of higher-order abstract syntax, LICS 1999 [ieee:782616, doi:10.1109/LICS.1999.782616]
Marcelo Fiore, Gordon Plotkin, Daniele Turi. Abstract syntax and variable binding, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158). IEEE (1999) [doi:10.1109/LICS.1999.782615, pdf, webpage]
Marcelo Fiore, Chung-Kil Hur. Second-order equational logic, International Workshop on Computer Science Logic. Springer, Lecture Notes in Computer Science 6247 (2010) [doi:10.1007/978-3-642-15205-4_26, pdf]
See also:
Last revised on January 5, 2023 at 18:18:19. See the history of this page for a list of all contributions to it.